| Definitions | False, P   Q,  A,  x:A. B(x), left + right, P  Q, Dec(P), ma-interface-consistent(es;X), [[I|i]], t  T, e  X,  b, x:A  B(x), E, ma-interface-consistent2(es;I), Id, MaInterface(T), Type, ES, Knd, ma-interface-dom(I;i), kind(e), (x l), hasloc(k;i), {x:A| B(x)} , x:A  B(x), a:A fp B(a), Atom$n, s = t, a < b, e@i. P(e), t.1, if b then t else f fi , val(e), ma-interface-valtype(I;i;k), Top, Void,  , Unit, ff, tt, IdLnk, rcv(l,tg), locl(a), let x,y = A in B(x;y), EqDecider(T), EOrderAxioms(E; pred?; info), f(a), EState(T), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List,  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, constant_function(f;A;B), P & Q, acttype(e), rcvtype(e), case b of inl(x) => s(x) | inr(y) => t(y), valtype(e), S  T, vartype(i;x), ma-interface-ds(I;i), f(x)?z, P  Q, P Q,   x. t(x), State(ds), state@i, IdDeq, x.A(x), @i discrete ds, <a, b>,  , {T}, SQType(T), (state when e), suptype(S; T), ma-interface-code(I;i;k), do-apply(f;x), A c B, s ~ t |
